""" This module contains utilities using for verification 
"""
from snakes.nets import StateGraph
from pig.action import Action
from pig.context import PiContextGraph
from pig.graph import PiGraphBuilder
from pig.name import Guard
from trans import NetTranslator

class PigUtils(object):
    """ Utilities used for pi-graph. 
    """
    def __init__(self):
        pass
    
    def printReplicator(self, r):
        print "%s[%d]" % (r.getName(), r.bound())
        print "Actions:"
        nodes = r.getNode()
        for n in nodes:
            print "%3d: %s" % (n, r.getNode(n))
        print "Connections:"
        nexts = r.getNext()
        for n in nexts.keys():
            print "%3d --> %s" % (n, r.getNext(n))
    
    def printPiGraph(self, gr):
        rnames = gr.getRepNames()
        print "============= Replicators ============="
        for rname in rnames:
            self.printReplicator(gr.getReplicator(rname))
        print "================ Names ================"
        gres = gr.getGresNames()
        if len(gres) > 0:
            print "* GRes: %s" % ",".join(str(n) for n in gres)
        frees = gr.freeNames()
        if len(frees) > 0:
            print "* Free: %s" % ", ".join(str(n) for n in frees)
        for rname in rnames:
            print "-------"
            tres = gr.tresNames(rname)
            if len(tres) > 0:
                print "* TRes of %s: %s" % (rname, ", ".join(str(n) for n in tres))
            varnames = gr.varNames(rname)
            if len(varnames) > 0:
                print "* Vars of %s: %s" % (rname, ", ".join(str(n) for n in varnames))
    
    def printState(self, stateObj, fhandle=None):
        """ Show a state
        """
        nc = stateObj.nameContext()
        namenv = nc.namenv()
        parts = nc.partitions()
        dists = nc.distinctions()
        if fhandle is None:
            print "\tBeta:  %r" % namenv
            print "\tGamma: %r" % parts
            print "\tDelta: %r" % dists
            
            cc = stateObj.ctrlContext()
            for m in cc.marking():
                rname = m.rname()
                gen = m.generator()
                dis = m.threads()
                print "\t::%s  Gen: {%r}\tIDs:%r" % (rname, gen, dis)
        else:
            fhandle.write("\tBeta:  %r\n\tGamma: %r\n\tDelta: %r\n" % (namenv, parts, dists))
            cc = stateObj.ctrlContext()
            for m in cc.marking():
                rname = m.rname()
                gen = m.generator()
                dis = m.threads()
                fhandle.write("\t::%s  Gen: {%r}\tIDs:%r\n" % (rname, gen, dis))
            
    def printStateGraph(self, sg, verbose=False, fhandle=None):
        """ Show a state graph of pi-graph
        """
        states = sg.getState()
        if verbose:
            for state in states:
                state_obj = sg.getState(state)
                succs = sg.getSuccessors(state)
                for x in succs:
                    actions = sg.getActions(state, x)
                    if fhandle is None:
                        print "-------------------"
                        print "* State %d:" % state
                    else:
                        fhandle.write("-------------------\n* State %d:\n" % state)
                    self.printState(state_obj, fhandle)
                    if fhandle is None:
                        print "\n  act:", "; ".join(str(act) for act in actions)
                        print "\n  State %d:" % x
                    else:
                        fhandle.write("  act:" + "; ".join(str(act) for act in actions))
                        fhandle.write("\n  State %d:\n" % x)
                    next_obj = sg.getState(x)
                    self.printState(next_obj, fhandle)
            if fhandle is None:
                print "-------------------------"
                if not sg.isCompleted():
                    print "Not completed!"
                print "Total: %d states" % sg.numOfStates()
            else:
                fhandle.write("-------------------------\n")
                if not sg.isCompleted():
                    fhandle.write("Not completed!\n")
                fhandle.write("Total: %d states" % sg.numOfStates())

        else:
            if fhandle is None:
                print "* States:"
                for state in states:
                    state_obj = sg.getState(state)
                    print "%3d:" % state
                    self.printState(state_obj)
                print "\n* Actions"
                for state in states:
                    succs = sg.getSuccessors(state)
                    for x in succs:
                        actions = sg.getActions(state, x)
                        print "%3d -->%3d:" % (state, x), "; ".join(str(act) for act in actions)
            else:
                fhandle.write("* States:\n")
                for state in states:
                    state_obj = sg.getState(state)
                    fhandle.write("%3d:\n" % state)
                    self.printState(state_obj, fhandle)
                fhandle.write("\n* Actions\n")
                for state in states:
                    succs = sg.getSuccessors(state)
                    for x in succs:
                        actions = sg.getActions(state, x)
                        fhandle.write("%3d -->%3d:" % (state, x))
                        fhandle.write("; ".join(str(act) for act in actions))
                        fhandle.write("\n")
    
    def checkPiStateGraph(self, s, verbose=False, fname=None):
        """ Check if there are how many states
        """
        bld = PiGraphBuilder()
        bld.inputSpec(s)
        g = bld.build()
        sg = PiContextGraph(g)
        n = sg.build(100000)  # maximum number of states
        fhandle = None
        if fname is not None:
            fhandle = open(fname, 'w')
        if verbose:
            if fhandle is None:
                print "\n============ Pi-graphs test ============"
            self.printStateGraph(sg, True, fhandle)  # FIXME: for test
        if fhandle is not None:
            fhandle.close()
        return n
    
    
class NetUtils:
    def __init__(self):
        pass
    
    def isActPlace(self, pname):
        return pname.startswith("a")
    
    def netAction(self, net, tname):
        for name in net.pre(tname):
            if self.isActPlace(name):
                pname = name
                break
        actplace = net.place(pname)
        act = actplace.tokens.items()[0]
        return act
    
    def printNameContext(self, nc):
        """ Show a name context
        """
        namenv = nc.namenv()
        parts = nc.partitions()
        dists = nc.distinctions()
        print "\tBeta:  %r" % namenv
        print "\tGamma: %r" % parts
        print "\tDelta: %r" % dists
    
    def toNet(self, s):
        """ Translate a pi-graph specification into a Petri net
        """
        nt = NetTranslator()
        nt.inputSpec(s)
        return nt.translate()
    
    def checkGlobals(self, net):
        print '\nGlobals:'
        d = net.globals
        for k, v in d:
            if isinstance(v, Action):
                print k, 'Action'
            elif isinstance(v, Guard):
                print k, 'Guard'
            else:
                print '?'
                
    def checkPlaces(self, net):
        """ Show name of all places
        @param net: the net to be showed
        """
        count = 0
        print "\n* Places:"
        places = []
        for p in net.place():
            places.append(p.name)
        places.sort()
        for p in places:
            count = count + 1
            print "%3d. %s" % (count, p)
                                
    def checkTransitions(self, net, verbose=False):
        """ Show all transition of a net
        @param net: the net to be showed
        @param verbose:
            True: show all details
            False: hide all details
        """
        print "\n* Transitions:"
        count = 0
        if verbose:
            for t in net.transition():
                count = count + 1                
                source = ", ".join("%s{%s}" % (place, label) for place, label in t.pre.items())
                post = {}
                for place, label in t.post.items():
                    s = str(label)
                    if s.find(".") != -1:
                        s = s.split(".")[1]
                    post[place] = s
                target = ", ".join("{%s}%s" % (label, place) for place, label in post.items())
                templ = "%3d. %s: %s\n\t%s \n\t    %s -> \n\t%s"
                act = self.netAction(net, t.name)
                s = templ % (count, t, act, source, str(t.guard).split(".")[1], target)
                print s, "\n"
        else:
            for t in net.transition():
                count = count + 1
                tname = t.name
                source = ", ".join("%s" % p for p in net.pre(tname))
                target = ", ".join("%s" % p for p in net.post(tname))
                print "%3d. %s -> %s -> %s\n" % (count, source, net.globals[tname], target)
    
    def checkNetStructure(self, s, verbose=False):
        """ Show the structure of translated net
        """
        p = NetTranslator()
        p.inputSpec(s)
        n = p.translate()
        print "\n============ Net structure ============"
        self.checkPlaces(n)
        self.checkTransitions(n, verbose)
            
    def checkNetStateGraph(self, s, verbose=False):
        """ Check there are how many states
        """
        p = NetTranslator()
        p.inputSpec(s)
        n = p.translate()
        g = StateGraph(n)
        count = 0
        if verbose:
            print "\n============ Net state graph test ============"
            for s in g:
                m = g.net.get_marking()
                print "%3s:" % s
                G = None
                for (p, tokens) in m.iteritems():
                    if p != "pG":
                        print "     %s = %s" % (p, tokens)
                    else:
                        for tk in tokens:
                            G = tk
                print "     pG ="
                self.printNameContext(G)
                count = count + 1
            print "-------------------"
            print "Total: %d states" % count
        else:
            for s in g:
                count = count + 1
        return count
    
class Checker(PigUtils, NetUtils):
    def __init__(self):
        pass
    
    def check(self, s):
        """ Check if the number of states of two model are equal
        """
        m = self.checkNetStateGraph(s)
        n = self.checkPiStateGraph(s)
        return m == n
    
    def checkAll(self, s):
        """ Check all information
        """
        self.checkPiStateGraph(s, True)
        self.checkNetStructure(s, True)
        self.checkNetStateGraph(s, True)
